Step of Proof: bnot_of_le_int
9,38
postcript
pdf
Inference at
*
1
I
of proof for Lemma
bnot
of
le
int
:
1.
i
:
2.
j
:
(
i
z
j
) =
j
<z
i
latex
by Unfold `le_int` 0
latex
1
:
1:
(
j
<z
i
) =
j
<z
i
.
Definitions
i
z
j
origin
(
i 
z j) = j <z i
by Unfold `le_int` 0
1:
1: (j <z i) = j <z i
.
(i z j) = j <z i
by Unfold `le_int` 0
1:
1: (j <z i) = j <z i
.z j